;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

(CL:IN-PACKAGE "STELLA")

(IN-MODULE "/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM")

(IN-DIALECT :KIF)

(set-feature iterative-deepening)

;------------------------------------------------------------------------------
; Basic Definitions
;------------------------------------------------------------------------------

(DEFRELATION  j   ((?x Being) (?y Being))) (ASSERT (closed j))

;------------------------------------------------------------------------------
; Axioms
;------------------------------------------------------------------------------

; AP1
(ASSERT (
	FORALL ((?x Being) (?y Being)) ( 
		<=>
			(j ?x ?y)
			(FORALL ((?z Being)) (
				=> (j ?z ?x) (j ?z ?y)
			))
	)
))

; AK1
(ASSERT (
	AND 
		(FORALL ((?y Being)) (EXISTS ((?x Being)) (
					NOT (j ?x ?y)
		)))
		(FORALL ((?x Being)) (EXISTS ((?y Being)) (
					NOT (j ?x ?y)
		)))
))

;------------------------------------------------------------------------------
; Aristotle Definitions
;------------------------------------------------------------------------------

(DEFRELATION  i   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(j ?z ?x)
			(j ?z ?y)
	)
)) (ASSERT (closed i))

(DEFRELATION  a   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(j ?z ?x)
			(i ?z ?y)
	)
)) (ASSERT (closed a))

(DEFRELATION  e   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(j ?z ?x)
			(NOT (j ?z ?y))
	)		
)) (ASSERT (closed e))

(DEFRELATION  o   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(j ?z ?x)
			(e ?z ?y)
	)		
)) (ASSERT (closed o))

;------------------------------------------------------------------------------
; Additional Definitions
;------------------------------------------------------------------------------

(DEFRELATION  eq  ((?x Being) (?y Being))
:<=> (
	AND (a ?x ?y) (a ?y ?x)
)) (ASSERT (closed eq))

(DEFFUNCTION  ng  ((?x Being)):->(?b Being)) (ASSERT (total ng))
(ASSERT (
	FORALL ((?x Being) (?y Being)) (
		<=>
			(j ?x (ng ?y))
			(e ?x ?y)
	)
))